eajs.5.jani:model: info: eajs.5 is an MDP model.
eajs.5.jani:variables[11]: info: Expanding variable "loc_1" into 3 locations in automaton "Process_1".
eajs.5.jani:variables[15]: info: Expanding variable "loc_2" into 3 locations in automaton "Process_2".
eajs.5.jani:variables[17]: info: Expanding variable "user_1" into 6 locations in automaton "Resources".
eajs.5.jani:variables[19]: info: Expanding variable "loc_3" into 3 locations in automaton "Process_3".
eajs.5.jani:variables[20]: info: Expanding variable "loc_5" into 3 locations in automaton "Process_5".
eajs.5.jani:variables[23]: info: Expanding variable "loc_4" into 3 locations in automaton "Process_4".
eajs.5.jani: info: Need 24 bytes per state.
eajs.5.jani: warning: The probabilities for a transition do not sum up to 1. Results will likely be affected by floating-point errors.
eajs.5.jani: info: Explored 3049471 states for energy_capacity=250, B=11.
Peak memory usage: 1332 MB
Analysis results for eajs.5.jani
Experiment energy_capacity=250, B=11
+ State space exploration
State size: 24 bytes
States: 3049471
Transitions: 4250853
Branches: 6960278
Rate: 261465 states/s
Time: 12.1 s
+ Property ExpUtil
Value: 10.032940688435431
Bounds: [10.032940688435431, infinity)
Time: 4.9 s
+ Precomputations
Min. prob. 0 states: 0
Time for min. prob. 0 states: 1.9 s
Min. prob. 1 states: 3049471
Time for min. prob. 1 states: 0.2 s
+ Essential states
Iterations: 4
Essential states: 1432081
Transitions: 2633463
Branches: 5342888
Time: 1.1 s
+ Value iteration
Final error: 8.368421047965715E-07
Iterations: 16
Time: 1.6 s
Exported results to file "/out.txt".